#include <iostream>
#include <vector>
using namespace std;
#include "cfa.h"

/*build a program with c--
program is under
main(){
    r = 1;
    a = 4;
    b = 7;
    r = gcd(a, b);
    assert(r = 1);
}
gcd(int a, int b){
    if(a > b){
        gcd(a-b, b);
    }
    if(a < b){
        gcd(a, b-a);
    }
    if(a = b){
        r = a;
    }
    return r;
}
*/
vector<CFA> testcfa1(){
    vector<CFA> result;
    CFA cfa1, cfa2;

    Node *x1, *x2, *x3, *x4, *x5, *x6, *x7;
    Expr *e1, *e2, *e3, *e4, *e5, *e6, *e7, *e8;
    Prop *p1;
    //r = 1
    x1 = new UniNode;
    e1 = new VarExpr;
    strcpy(((VarExpr*)e1)->s, "r");
    strcpy(((UniNode*)x1)->statement, "r=1;");
    e2 = new IntExpr;
    ((IntExpr*)e2)->i = 1;
    ((UniNode*)x1)->e1 = e1;
    ((UniNode*)x1)->e2 = e2;
    //a = 4
    x2 = new UniNode;
    e3 = new VarExpr;
    strcpy(((VarExpr*)e3)->s, "a");
    strcpy(((UniNode*)x2)->statement, "a=1;");
    e4 = new IntExpr;
    ((IntExpr*)e4)->i = 1;
    ((UniNode*)x2)->e1 = e3;
    ((UniNode*)x2)->e2 = e4;
    ((UniNode*)x1)->next = x2;
    cfa1.SetInitNode(x1);
    //b = 7
    x3 = new UniNode;
    e5 = new VarExpr;
    strcpy(((VarExpr*)e5)->s, "b");
    strcpy(((UniNode*)x3)->statement, "b=7;");
    e6 = new IntExpr;
    ((IntExpr*)e6)->i = 7;
    ((UniNode*)x3)->e1 = e5;
    ((UniNode*)x3)->e2 = e6;
    ((UniNode*)x2)->next = x3;
    //gcd
    x4 = new UniNode;
    strcpy(((UniNode*)x4)->statement, "gcd(a, b)");
    ((UniNode*)x4)->e1 = NULL;
    ((UniNode*)x4)->e2 = NULL;
    ((UniNode*)x3)->next = x4;
    //assert(r=1);
    x5 = new BinNode;
    p1 = new InequProp;
    e7 = new VarExpr;
    strcpy(((VarExpr*)e7)->s, "r");
    e8 = new IntExpr;
    ((IntExpr*)e8)->i = 1;
    ((InequProp*)p1)->p = Eq;
    ((InequProp*)p1)->e1 = e7;
    ((InequProp*)p1)->e2 = e8;
    ((BinNode*)x5)->p = p1;
    ((UniNode*)x4)->next = x5;
    //terminal node
    x6 = new TermNode;
    ((BinNode*)x5)->next1 = x6;
    x7 = new BadNode;
    ((BinNode*)x5)->next2 = x7;
    //function gcd
    Node *y1, *y2, *y3, *y4, *y5, *y6, *y7, *y8, *y9, *y10;
    Expr *d1, *d2, *d3, *d4_2, *d5, *d6, *d7, *d8, *d9, *d10, *d11, *d12;
    Prop *q1, *q2, *q3;
    //a = 4;
    y1 = new UniNode;
    d1 = new VarExpr;
    d2 = new IntExpr;
    strcpy(((VarExpr*)d1)->s, "a");
    ((IntExpr*)d2)->i = 4;
    ((UniNode*)y1)->e1 = d1;
    ((UniNode*)y1)->e2 = d2;
    strcpy(((UniNode*)y1)->statement, "a=4;");
    //b=7
    y2 = new UniNode;
    d3 = new VarExpr;
    strcpy(((VarExpr*)d3)->s, "b");
    //d4_1 = new BinExpr;
    //((BinExpr*)d4_1)->e1 = d3;
    d4_2 = new IntExpr;
    ((IntExpr*)d4_2)->i = 7;
    //((BinExpr*)d4_1)->e2 = d4_2;
    //((BinExpr*)d4_1)->op = Plus;
    ((UniNode*)y2)->e1 = d3;
    ((UniNode*)y2)->e2 = d4_2;
    strcpy(((UniNode*)y2)->statement, "b=7;");
    ((UniNode*)y1)->next = y2;
    cfa2.SetInitNode(y1);
    //a > b
    y3 = new BinNode;
    d5 = new VarExpr;
    d6 = new VarExpr;
    q1 = new InequProp;
    strcpy(((VarExpr*)d5)->s, "a");
    strcpy(((VarExpr*)d6)->s, "b");
    ((InequProp*)q1)->p = GT;
    ((InequProp*)q1)->e1 = d5;
    ((InequProp*)q1)->e2 = d6;
    ((BinNode*)y3)->p = q1;
    ((UniNode*)y2)->next = y3;
    //gcd(a-b)
    y4 = new UniNode;
    ((UniNode*)y4)->e1 = NULL;
    ((UniNode*)y4)->e2 = NULL;
    strcpy(((UniNode*)y4)->statement, "gcd(a-b, b)");
    ((BinNode*)y3)->next1 = y4;
    //a < b
    y5 = new BinNode;
    d7 = new VarExpr;
    d8 = new VarExpr;
    q2 = new InequProp;
    strcpy(((VarExpr*)d7)->s, "a");
    strcpy(((VarExpr*)d8)->s, "b");
    ((InequProp*)q2)->p = LT;
    ((InequProp*)q2)->e1 = d7;
    ((InequProp*)q2)->e2 = d8;
    ((BinNode*)y5)->p = q2;
    ((UniNode*)y4)->next = y5;
    ((BinNode*)y3)->next2 = y5;
    //gcd()
    y6 = new UniNode;
    ((UniNode*)y6)->e1 = NULL;
    ((UniNode*)y6)->e2 = NULL;
    strcpy(((UniNode*)y6)->statement, "gcd(a, a-b)");
    ((BinNode*)y5)->next1 = y6;
    //a=b
    y7 = new BinNode;
    d9 = new VarExpr;
    d10 = new VarExpr;
    q3 = new InequProp;
    strcpy(((VarExpr*)d9)->s, "a");
    strcpy(((VarExpr*)d10)->s, "b");
    ((InequProp*)q3)->p = Eq;
    ((InequProp*)q3)->e1 = d9;
    ((InequProp*)q3)->e2 = d10;
    ((BinNode*)y7)->p = q3;
    ((UniNode*)y6)->next = y7;
    ((BinNode*)y5)->next2 = y7;
    //r=a
    y8 = new UniNode;
    d11 = new VarExpr;
    d12 = new VarExpr;
    strcpy(((VarExpr*)d11)->s, "r");
    strcpy(((VarExpr*)d12)->s, "a");
    strcpy(((UniNode*)y8)->statement, "r=a;");
    ((UniNode*)y8)->e1 = d11;
    ((UniNode*)y8)->e2 = d12;
    ((BinNode*)y7)->next1 = y8;
    //retrun r;
    y9 = new UniNode;
    ((UniNode*)y9)->e1 = NULL;
    ((UniNode*)y9)->e2 = NULL;
    strcpy(((UniNode*)y9)->statement, "return r");
    ((UniNode*)y8)->next = y9;
    ((BinNode*)y7)->next2 = y9;
    //termnode
    y10 = new TermNode;
    ((UniNode*)y9)->next = y10;
    result.push_back(cfa1);
    result.push_back(cfa2);
    return result;
}
/*
i1 = 1;
i2 = 1;
while(n < 20){
    i3 = i1 + i2;
    i1 = i2;
    i2 = i3;
    assert(n < 19);
    n = n + 1;
}
*/
vector<CFA> testcfa2(){
    vector<CFA> result;
    CFA cfa1;
  
    Node *a1, *a2, *a3, *a4, *a5, *a6, *a7, *a8, *a9, *a10;
    Expr *ex1_1, *ex1_2, *ex2_1, *ex2_2, *ex3_1, *ex3_2, *ex4_1, *ex4_2, *ex4_3, *ex4_4, *ex5_1, *ex5_2, *ex6_1, *ex6_2, *ex7_1, *ex7_2, *ex8_1, *ex8_2, *ex8_3;
    Prop *pr1_1, *pr2_1;
    //i1 = 1;
    a1 = new UniNode;
    ex1_1 = new VarExpr;
    ex1_2 = new IntExpr;
    strcpy(((VarExpr*)ex1_1)->s, "i1");
    ((IntExpr*)ex1_2)->i = 1;
    ((UniNode*)a1)->e1 = ex1_1;
    ((UniNode*)a1)->e2 = ex1_2;
    strcpy(((UniNode*)a1)->statement, "i1=1;");
    //i2 = 1;
    a2 = new UniNode;
    ex2_1 = new VarExpr;
    ex2_2 = new IntExpr;
    strcpy(((VarExpr*)ex2_1)->s, "i2");
    ((IntExpr*)ex2_2)->i = 1;
    ((UniNode*)a2)->e1 = ex2_1;
    ((UniNode*)a2)->e2 = ex2_2;
    strcpy(((UniNode*)a2)->statement, "i2=1;");
    ((UniNode*)a1)->next = a2;
    cfa1.SetInitNode(a1);
    //n<20
    a3 = new BinNode;
    pr1_1 = new InequProp;
    ex3_1 = new VarExpr;
    ex3_2 = new IntExpr;
    strcpy(((VarExpr*)ex3_1)->s, "n");
    ((IntExpr*)ex3_2)->i = 20;
    ((InequProp*)pr1_1)->p = LT;
    ((InequProp*)pr1_1)->e1 = ex3_1;
    ((InequProp*)pr1_1)->e2 = ex3_2;
    ((BinNode*)a3)->p = pr1_1;
    ((UniNode*)a2)->next = a3;
    //i3 = i1 + i2;
    a4 = new UniNode;
    ex4_1 = new VarExpr;
    ex4_2 = new VarExpr;
    ex4_3 = new VarExpr;
    ex4_4 = new BinExpr;
    strcpy(((VarExpr*)ex4_1)->s, "i3");
    strcpy(((VarExpr*)ex4_2)->s, "i1");
    strcpy(((VarExpr*)ex4_3)->s, "i2");
    ((BinExpr*)ex4_4)->op = Plus;
    ((BinExpr*)ex4_4)->e1 = ex4_2;
    ((BinExpr*)ex4_4)->e2 = ex4_3;
    ((UniNode*)a4)->e1 = ex4_1;
    ((UniNode*)a4)->e2 = ex4_4;
    strcpy(((UniNode*)a4)->statement, "i3=i1+i2;");
    ((BinNode*)a3)->next1 = a4;
    //i1 = i2;
    a5 = new UniNode;
    ex5_1 = new VarExpr;
    ex5_2 = new VarExpr;
    strcpy(((VarExpr*)ex5_1)->s, "i1");
    strcpy(((VarExpr*)ex5_2)->s, "i2");
    ((UniNode*)a5)->e1 = ex5_1;
    ((UniNode*)a5)->e2 = ex5_2;
    strcpy(((UniNode*)a5)->statement, "i1=i2;");
    ((UniNode*)a4)->next = a5;
    //i2 = i3
    a6 = new UniNode;
    ex6_1 = new VarExpr;
    ex6_2 = new VarExpr;
    strcpy(((VarExpr*)ex6_1)->s, "i2");
    strcpy(((VarExpr*)ex6_2)->s, "i3");
    ((UniNode*)a6)->e1 = ex6_1;
    ((UniNode*)a6)->e2 = ex6_2;
    strcpy(((UniNode*)a6)->statement, "i2=i3;");
    ((UniNode*)a5)->next = a6;
    // n < 9
    a7 = new BinNode;
    pr2_1 = new InequProp;
    ex7_1 = new VarExpr;
    ex7_2 = new IntExpr;
    strcpy(((VarExpr*)ex7_1)->s, "n");
    ((IntExpr*)ex7_2)->i = 9;
    ((InequProp*)pr2_1)->p = LT;
    ((InequProp*)pr2_1)->e1 = ex3_1;
    ((InequProp*)pr2_1)->e2 = ex3_2;
    ((BinNode*)a7)->p = pr2_1;
    ((UniNode*)a6)->next = a7;
    // n = n + 1
    a8 = new UniNode;
    ex8_1 = new VarExpr;
    ex8_2 = new IntExpr;
    ex8_3 = new BinExpr;
    strcpy(((VarExpr*)ex8_1)->s, "n");
    ((IntExpr*)ex8_2)->i = 1;
    ((BinExpr*)ex8_3)->op = Plus;
    ((BinExpr*)ex8_3)->e1 = ex8_1;
    ((BinExpr*)ex8_3)->e2 = ex8_2;
    ((UniNode*)a8)->e1 = ex8_1;
    ((UniNode*)a8)->e2 = ex8_3;
    strcpy(((UniNode*)a8)->statement, "n=n+1;");
    ((BinNode*)a7)->next1 = a8;
    //termnode badnode
    a9 = new BadNode;
    ((BinNode*)a7)->next2 = a9;
    a10 = new TermNode;
    ((BinNode*)a3)->next2 = a10;
    //loop
    ((UniNode*)a8)->next = a3;
    result.push_back(cfa1);
    return result;
}
/*
x1 = 1;
x2 = 0;
r1 = 0;
while(x1 < 10){
    x2 = 1;
    while(x2 < 10){
        x2 = x2 + 1;
        assert(x2 < 9);
    }
    x1 = x1 + 1;
    assert(x1 < 9);
}
*/
vector<CFA> testcfa3(){
    vector<CFA> result;
    CFA cfa1;
  
    Node *a1, *a2, *a3, *a4, *a5, *a6, *a7, *a8, *a9, *a10, *a11, *a12;
    Expr *ex1_1, *ex1_2, *ex2_1, *ex2_2, *ex3_1, *ex3_2, *ex4_1, *ex4_2, *ex5_1, *ex5_2, *ex6_1, *ex6_2, *ex7_1, *ex7_2, *ex7_3, *ex8_1, *ex8_2, *ex9_1, *ex9_2, *ex9_3, *ex10_1, *ex10_2;
    Prop *pr1_1, *pr2_1, *pr3_1, *pr4_1;
    //x1 = 1;
    a1 = new UniNode;
    ex1_1 = new VarExpr;
    ex1_2 = new IntExpr;
    strcpy(((VarExpr*)ex1_1)->s, "x1");
    ((IntExpr*)ex1_2)->i = 1;
    ((UniNode*)a1)->e1 = ex1_1;
    ((UniNode*)a1)->e2 = ex1_2;
    strcpy(((UniNode*)a1)->statement, "x1=1;");
    //x2 = 0;
    a2 = new UniNode;
    ex2_1 = new VarExpr;
    ex2_2 = new IntExpr;
    strcpy(((VarExpr*)ex2_1)->s, "x2");
    ((IntExpr*)ex2_2)->i = 0;
    ((UniNode*)a2)->e1 = ex2_1;
    ((UniNode*)a2)->e2 = ex2_2;
    strcpy(((UniNode*)a2)->statement, "x2=0;");
    ((UniNode*)a1)->next = a2;
    cfa1.SetInitNode(a1);
    //r1 = 0
    a3 = new UniNode;
    ex3_1 = new VarExpr;
    ex3_2 = new IntExpr;
    strcpy(((VarExpr*)ex3_1)->s, "r1");
    ((IntExpr*)ex2_2)->i = 0;
    ((UniNode*)a3)->e1 = ex3_1;
    ((UniNode*)a3)->e2 = ex2_2;
    strcpy(((UniNode*)a3)->statement, "r1=0;");
    ((UniNode*)a2)->next = a3;
    //x1 < 10
    a4 = new BinNode;
    pr1_1 = new InequProp;
    ex4_1 = new VarExpr;
    ex4_2 = new IntExpr;
    strcpy(((VarExpr*)ex4_1)->s, "x1");
    ((IntExpr*)ex4_2)->i = 10;
    ((InequProp*)pr1_1)->p = LT;
    ((InequProp*)pr1_1)->e1 = ex4_1;
    ((InequProp*)pr1_1)->e2 = ex4_2;
    ((BinNode*)a4)->p = pr1_1;
    ((UniNode*)a3)->next = a4;
    //x2 = 1;
    a5 = new UniNode;
    ex5_1 = new VarExpr;
    ex5_2 = new IntExpr;
    strcpy(((VarExpr*)ex5_1)->s, "x2");
    ((IntExpr*)ex5_2)->i = 1;
    ((UniNode*)a5)->e1 = ex5_1;
    ((UniNode*)a5)->e2 = ex5_2;
    strcpy(((UniNode*)a5)->statement, "x2=1;");
    ((BinNode*)a4)->next1 = a5;
    //x2 < 10
    a6 = new BinNode;
    pr2_1 = new InequProp;
    ex6_1 = new VarExpr;
    ex6_2 = new IntExpr;
    strcpy(((VarExpr*)ex6_1)->s, "x2");
    ((IntExpr*)ex6_2)->i = 10;
    ((InequProp*)pr2_1)->p = LT;
    ((InequProp*)pr2_1)->e1 = ex6_1;
    ((InequProp*)pr2_1)->e2 = ex6_2;
    ((BinNode*)a6)->p = pr2_1;
    ((UniNode*)a5)->next = a6;
    //x2=x2+1
    a7 = new UniNode;
    ex7_1 = new VarExpr;
    ex7_2 = new IntExpr;
    ex7_3 = new BinExpr;
    strcpy(((VarExpr*)ex7_1)->s, "x2");
    ((IntExpr*)ex7_2)->i = 1;
    ((BinExpr*)ex7_3)->op = Plus;
    ((BinExpr*)ex7_3)->e1 = ex7_1;
    ((BinExpr*)ex7_3)->e2 = ex7_2;
    ((UniNode*)a7)->e1 = ex7_1;
    ((UniNode*)a7)->e2 = ex7_3;
    strcpy(((UniNode*)a7)->statement, "x2=x2+1;");
    ((BinNode*)a6)->next1 = a7;
    //x2 < 9
    a8 = new BinNode;
    pr3_1 = new InequProp;
    ex8_1 = new VarExpr;
    ex8_2 = new IntExpr;
    strcpy(((VarExpr*)ex8_1)->s, "x2");
    ((IntExpr*)ex8_2)->i = 9;
    ((InequProp*)pr3_1)->p = LT;
    ((InequProp*)pr3_1)->e1 = ex8_1;
    ((InequProp*)pr3_1)->e2 = ex8_2;
    ((BinNode*)a8)->p = pr3_1;
    ((UniNode*)a7)->next = a8;
    //x1=x1+!
    a9 = new UniNode;
    ex9_1 = new VarExpr;
    ex9_2 = new IntExpr;
    ex9_3 = new BinExpr;
    strcpy(((VarExpr*)ex9_1)->s, "x1");
    ((IntExpr*)ex9_2)->i = 1;
    ((BinExpr*)ex9_3)->op = Plus;
    ((BinExpr*)ex9_3)->e1 = ex9_1;
    ((BinExpr*)ex9_3)->e2 = ex9_2;
    ((UniNode*)a9)->e1 = ex9_1;
    ((UniNode*)a9)->e2 = ex9_3;
    strcpy(((UniNode*)a9)->statement, "x1=x1+1;");
    ((BinNode*)a8)->next1 = a6;
    ((BinNode*)a6)->next2 = a9;
    //x1<9
    a10 = new BinNode;
    pr4_1 = new InequProp;
    ex10_1 = new VarExpr;
    ex10_2 = new IntExpr;
    strcpy(((VarExpr*)ex10_1)->s, "x1");
    ((IntExpr*)ex10_2)->i = 9;
    ((InequProp*)pr4_1)->p = LT;
    ((InequProp*)pr4_1)->e1 = ex10_1;
    ((InequProp*)pr4_1)->e2 = ex10_2;
    ((BinNode*)a10)->p = pr4_1;
    ((UniNode*)a9)->next = a10;
    ((BinNode*)a10)->next1 = a4;
    //Termnode BadNode;
    a11 = new TermNode;
    ((BinNode*)a4)->next2 = a11;
    a12 = new BadNode;
    ((BinNode*)a10)->next2 = a12;
    ((BinNode*)a8)->next2 = a12;
    //cfa
    result.push_back(cfa1);
    return result;
}
